; <lemma>
;  <title>ch7_conc.28</title>
;  <origin>ch7_conc | conc_2 | Writer_42/inv10/INV</origin>
(benchmark ch7_conc_28
;  <theories>
;    <theory name="linear_order_int"/>
;    <theory name="basic_set"/>
;  </theories>
  :logic AUFLIA
;  <typenv>
;    <variable name="w" type="INTEGER"/>
;  </typenv>
  :extrafuns ((w Int)(m Int))
  :extramacros (
		 (Nat (lambda (?i Int) . (<= 0 ?i)))
		 (in (lambda (?x1 't1) (?p ('t1 boolean)) . (?p ?x1)))
		 (range (lambda (?i1 Int) (?i2 Int) .
			  (lambda (?i Int) .
			    (and (<= ?i1 ?i) (<= ?i ?i2)))))
		 (ismax
		   (lambda (?m Int) (?pi (Int boolean))  .
		     (and (?pi ?m)
		       (forall (?i1 Int) . (implies (?pi ?i1) (<= ?i1 ?m))))))
		 )
; <hypothesis needed="true">w : NATURAL</hypothesis>
  :assumption (in w Nat)
; m <--> max(1 .. w+1)
  :assumption (ismax m (range 1 (+ w 1)))
; <goal>max(1 .. w+1) = w+1</goal>
  :formula
  (not
      (= m (+ w 1))
    )
)
; </lemma>
